Nuprl Lemma : qless_is_sp_of_leq_a_qorder 11,40
a, b:. a < b  (a  b & (b  a)) 
latex

Definitionsx,y. t(x;y), , x f y, t  T, OMon, t.1, Mon, x(s1,s2), AbMon, OCMon, OGrp, <+>, |g|, P & Q, x:A. B(x), r  s, r < s
Lemmasocgrp wf, grp le wf, assert wf, grp car wf, linorder wf, qadd grp wf2, grp lt is sp of leq a

origin